#include "PDTExpBoolBinBoolDerived.h"
#include "PDTCodeGraph.h"
#include "PDTZ3GraphVisitor.h"

PDTAnd::PDTAnd(PDTCodeGraph & CG, PDTExpBool &left, PDTExpBool & right) :
	PDTExpBoolBinBool(CG, left, right) {
}

Z3_ast
PDTAnd::Z3NodeVisit (PDTZ3Visitor &ZV)
{
    if (Z3node != NULL)
        return Z3node;

    Z3_ast child1 = getLeft()->Z3visit(ZV);
    Z3_ast child2 = getRight()->Z3visit(ZV);

    Z3_ast args[2];
    args[0] = child1;
    args[1] = child2;

    Z3node = Z3_mk_and(ZV.ctx,2,args);
    return Z3node;
}


PDTOr::PDTOr(PDTCodeGraph & CG, PDTExpBool &left, PDTExpBool & right) :
	PDTExpBoolBinBool(CG, left, right) {
}

Z3_ast
PDTOr::Z3NodeVisit (PDTZ3Visitor &ZV)
{
    if (Z3node != NULL)
        return Z3node;

    Z3_ast child1 = getLeft()->Z3visit(ZV);
    Z3_ast child2 = getRight()->Z3visit(ZV);

    Z3_ast args[2];
    args[0] = child1;
    args[1] = child2;

    Z3node = Z3_mk_or(ZV.ctx,2,args);
    return Z3node;
}

PDTEqualBool::PDTEqualBool(PDTCodeGraph & CG, PDTExpBool &left,
		PDTExpBool & right) :
	PDTExpBoolBinBool(CG, left, right) {
}

Z3_ast
PDTEqualBool::Z3NodeVisit (PDTZ3Visitor &ZV)
{
    if (Z3node != NULL)
        return Z3node;

    Z3_ast child1 = getLeft()->Z3visit(ZV);
    Z3_ast child2 = getRight()->Z3visit(ZV);

    assert( Z3_get_sort(ZV.ctx, child1) == Z3_get_sort(ZV.ctx,child2));
    assert( Z3_get_sort(ZV.ctx, child1) == ZV.Bool);

    Z3node = Z3_mk_eq(ZV.ctx,child1,child2);
    return Z3node;
}


PDTNotEqualBool::PDTNotEqualBool(PDTCodeGraph & CG, PDTExpBool &left,
		PDTExpBool & right) :
	PDTExpBoolBinBool(CG, left, right) {
}

Z3_ast
PDTNotEqualBool::Z3NodeVisit (PDTZ3Visitor &ZV)
{
    if (Z3node != NULL)
        return Z3node;

    Z3_ast child1 = getLeft()->Z3visit(ZV);
    Z3_ast child2 = getRight()->Z3visit(ZV);

    assert( Z3_get_sort(ZV.ctx, child1) == Z3_get_sort(ZV.ctx,child2));
    assert( Z3_get_sort(ZV.ctx, child1) == ZV.Bool);

	Z3_ast args[2];
	args[0] = child1;
	args[1] = child2;

    Z3node = Z3_mk_distinct(ZV.ctx,2,args);
    return Z3node;
}


PDTXor::PDTXor(PDTCodeGraph & CG, PDTExpBool &left, PDTExpBool & right) :
	PDTExpBoolBinBool(CG, left, right) 
{
}


Z3_ast
PDTXor::Z3NodeVisit (PDTZ3Visitor &ZV)
{
    if (Z3node != NULL)
        return Z3node;

    Z3_ast child1 = getLeft()->Z3visit(ZV);
    Z3_ast child2 = getRight()->Z3visit(ZV);

    assert( Z3_get_sort(ZV.ctx, child1) == Z3_get_sort(ZV.ctx,child2));
    assert( Z3_get_sort(ZV.ctx, child1) == ZV.Bool);

    Z3node = Z3_mk_xor(ZV.ctx,child1,child2);
    return Z3node;
}



PDTImplies::PDTImplies(PDTCodeGraph & CG, PDTExpBool &left, PDTExpBool & right) :
	PDTExpBoolBinBool(CG, left, right) {
}

Z3_ast
PDTImplies::Z3NodeVisit (PDTZ3Visitor &ZV)
{
    if (Z3node != NULL)
        return Z3node;

    Z3_ast child1 = getLeft()->Z3visit(ZV);
    Z3_ast child2 = getRight()->Z3visit(ZV);

    assert( Z3_get_sort(ZV.ctx, child1) == Z3_get_sort(ZV.ctx,child2));
    assert( Z3_get_sort(ZV.ctx, child1) == ZV.Bool);

    Z3node = Z3_mk_implies(ZV.ctx,child1,child2);
    return Z3node;
}
